(assert (forall ((q0 Int) (q1 Bool)) (=> (and q1 q1 q1 q1 q1) (= (mod (mod q0 q0) (mod q0 q0)) (mod q0 q0)))))
(assert (forall ((q5 Int) (q6 Int) (q7 Bool)) (=> (and q7 q7 q7 q7 q7 q7) (< (- q5 q5 q5 q6) (+ (- q5 q5 q5 q6) q5 q5)))))
(assert (forall ((q14 Int) (q15 Int) (q16 Int) (q17 Bool)) (=> (< q14 (mod q15 q16)) (and q17 q17))))
(declare-const i3 Int)
(assert (forall ((q25 Int) (q26 Int) (q27 Int) (q28 Bool)) (=> (not q28) (> q27 (div (mod (div q25 q27) q25) (div q25 q27))))))
(assert (forall ((q29 Int) (q30 Int) (q31 Int) (q32 Bool)) (=> (> q31 (div q29 q29)) (and q32 q32 q32 q32 q32 q32 q32 q32))))
(assert (forall ((q33 Int) (q34 Int) (q35 Bool)) (=> (and q35 q35 q35 q35 q35 q35 q35 q35 q35) (< q34 q33))))
(assert (forall ((q36 Int) (q37 Int) (q38 Bool)) (=> (=> q38 q38) (= q37 (div (mod (div q37 q36) q36) q36)))))
(check-sat)
